perm filename MULT[EKL,SYS]3 blob
sn#825733 filedate 1986-10-11 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 the notion of multiplicity
C00006 00003 multiplicity of union is sum of multiplicities
C00010 ENDMK
C⊗;
;the notion of multiplicity
(wipe-out)
(get-proofs sums prf ekl sys)
(proof multiplicity)
(decl mult (type: |(ground⊗@set)→ground|) (syntype: constant))
(defax mult |∀x u a.mult(nil,a)=0∧
mult(x.u,a)=if a(x) then mult(u,a)' else mult(u,a)|)
(label mult_def)
;facts about multiplicity
(axiom |∀u a.natnum(mult(u,a))|)
(label simpinfo)(label multfact)
(axiom |∀u a.mult(u,a)≤length(u)|)
(label length_mult)
(axiom |∀u y a.member(y,u)∧a(y)⊃1≤mult(u,a)|)
(label member_mult)
;Exercise:(not used in the proofs)
;(axiom |∀a u x.mult(u,a)≤mult(x.u,a)|)
;(label simpinfo)(label multfact)
(axiom |∀a u n.n<length(u)⊃mult(nthcdr(u,n),a)≤mult(u,a)|)
(label mult_nthcdr)
(axiom |∀u.mult(u,emptyset)=0|)
(label simpinfo)(label emptyfacts)
(axiom |∀v i j.i<j∧j<length v∧nth(v,i)=nth(v,j)⊃
2≤mult(v,mkset(nth(v,i)))|)
(label multinj_computation)
(axiom |∀v.(∀k.k<length v⊃mult(v,mkset(nth(v,k)))=1)⊃inj(v)|)
(label mult_inj)
;multiplicity of union is sum of multiplicities
(proof mult_of_un_is_sum_un)
(axiom |∀u a b.disj_pair(a,b)⊃mult(u,a∪b)=mult(u,a)+mult(u,b)|)
(label multsum)
(axiom |∀setseq u n.disjoint(setseq,n)⊃
mult(u,un(setseq,n))=sum(λm.mult(u,setseq(m)),n)|)
(label mult_of_un_is_sum_mult)
(save-proofs mult)